A:Type, f:(A(A + Top)). p-inject(A;A;f)  (n:. p-inject(A;A;f^n)) 

latex

ProofTree

Definitions	p-inject(A;B;f), Type, x:AB(x), , a < b, f^n, #$n, n - m, s = t, t  T, , x:A. B(x), P  Q, Top, left + right, {x:A| B(x)} , A  B, i  j , False, A, -n, n+m, Void, can-apply(f;x), p-id(), do-apply(f;x), b, True, , f o g  , x.A(x), primrec(n;b;c), f(a), ff, (i = j), , b, tt, x:A  B(x), P & Q, P  Q, x =a y, null(as), a < b, x f y, a < b, [d], p  q, p  q, p q, i <z j, i z j, Unit
Lemmas	eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, p-compose-inject, p-fun-exp wf, member wf, le wf, ge wf, nat properties, top wf, nat wf, nat ind tp, p-inject wf